
(* A prog is a list of decl and rules *)

open Mods

type ('info, 'node) node = { data : 'info;
			     node : 'node }

type 'info prog = 'info decl list * 'info proc_decl list * 'info rules (* DAVID : rules était avant proc_decl list, j'ai inversé *)

and loc = Lexing.position * Lexing.position

and ident = (loc, string) node
  
and 'info decl =
(*| Dconst of ident * 'info expr *)
| Dtype of ident * type_expr
| Dvar of var_decl

and var_decl = ident * type_expr 

(* TODO : a supprimer *)
and 'info alias = ident * 'info expr
  
and 'info rules = 'info rule list

and 'info designator = ('info, 'info designator_node) node
and 'info designator_node =
| DESid of ident
| DESarray of 'info designator * 'info expr
| DESdot of 'info designator * ident

and 'info rule = ('info, 'info rule_node) node
and 'info rule_node =
| Rsimple of 'info simplerule
| Rstart of 'info startstate
| Rinvariant of 'info invariant
| Rruleset of 'info ruleset

(* TODO : a supprimer *)
| Ralias of 'info aliasrule
| Rchoose of 'info chooserule (* DAVID : ajout de chooserule, pas dans la doc mais dans le code source de Murphi *)

and 'info simplerule = string option * 'info expr * 'info decl list * 'info stmts
    
and 'info startstate = string option * 'info decl list * 'info stmts

and 'info invariant = string option * 'info expr

and 'info ruleset = 'info quantifier list * 'info rules
(* DAVID : je pense que c'est quantifier list * rules au lieu de quantifier * quantifier list * rules *)

   
(* TODO : a supprimer *)
and 'info aliasrule = 'info alias list * 'info rules
(* DAVID : ce n'est pas alias * alias list * rules mais alias list * rules *)

and 'info chooserule = ident * 'info designator * 'info rules
(* DAVID : ajout de chooserule, pas dans la doc mais dans le code source de Murphi *)


(* REMY : Bien lu, désolé pour les erreurs. J'ai ajouté le option pour le optString dans l'ast aussi *)
    

    
and 'info stmts = 'info stmt list

(* Puteexpr : Don't ask what the first four letters means in french *)
and 'info putstmt = Putexpr of 'info expr | Putstring of string
    
and 'info stmt = ('info, 'info stmt_node) node
and 'info stmt_node =
| Sassign of 'info designator * 'info expr
| Sif of 'info expr * 'info stmts * 'info stmts
| Sswitch of 'info expr * ('info expr list * 'info stmts) list * 'info stmts
| Sfor of 'info quantifier list * 'info stmts
| Swhile of 'info expr * 'info stmts

(* TODO : a supprimer *)
| Salias of 'info alias list * 'info stmts
| Sproccall of ident * 'info expr list
| Sundef of 'info designator
| Serror of string
| Sclear of 'info designator
| Sassert of 'info expr * string option
| Sput of 'info putstmt
| Sreturn of 'info expr option
| Smultisetadd of 'info designator * 'info designator
| Smultisetremovepred of ident * 'info designator * 'info expr
| Smultisetremove of 'info expr * 'info designator
  
and type_expr =
| Tident of ident
| Tsubrange of int32 * int32
| Tint 
| Tenum of ident list
| Trecord of type_expr StrMap.t
(*| Trecord of var_decl list*)
| Tarray of type_expr * type_expr (* index * content *)
| Tscalarset of int32
| Tunion of type_expr list
| Tmultiset of int32 * type_expr
| Tany

and binop = Bplus | Bminus | Bmul | Bdiv | Bmod (* DAVID : tu avais mis Bpercent, je pense que Bmod est plus approprié *)
	    | Bor | Band | Bimplies | Blt | Bgt | Ble | Bge | Beq | Bne 

and 'info expr = ('info, 'info expr_node) node
and 'info expr_node = 
| Eforall of 'info quantifier list * 'info expr
| Eexists of 'info quantifier list * 'info expr
| Ebinop of binop * 'info expr * 'info expr
| Enot of 'info expr
| Econdition of 'info expr * 'info expr * 'info expr
| Edesignator of 'info designator
| Econst of int32
| Efuncall of ident * 'info expr list
| Eerror of string
| Emultiset_count of ident * 'info designator * 'info expr
| Eismem of 'info designator * type_expr
| Eisundef of 'info designator

and 'info quantifier = ('info, 'info quantifier_node) node
and 'info quantifier_node =
| Qvar of ident * type_expr
| Qfor of ident * 'info expr * 'info expr * 'info expr 

and 'info proc_decl
(* =
| Procedure_decl of procedure_decl
| Function_decl of function_decl
and procedure_decl = ident * formal list * decl * stmts
and formal 
*)







